Nuprl Lemma : conditional_wf-interface 11,40
es:ES, A, B:Type, Ia1, Ia2:AbsInterface(A), Ib1, Ib2:AbsInterface(B), g1:(E(Ib1)E(Ia1)),
g2:(E(Ib2)E(Ia2)).
[{Ib1}? g1 : g2]  {e:E| {[Ib1?Ib2]}(e)} {e:E| {[Ia1?Ia2]}(e)}  
latex

Definitionsx:A. B(x), AbsInterface(A), t  T, {I}, , P  Q, {T}, Top, E(X), P  Q, P  Q, P  Q, P & Q, A, False
Lemmases-interface-conditional, conditional wf, assert wf, es-is-interface wf, bool-decider wf, decidable wf, subtype rel function, es-interface-conditional-domain-iff, es-E-interface wf, subtype rel sum, es-E wf, top wf, es-interface wf, event system wf

origin